A, B:Knd, es:ES, T:Type, m:T.
((A = B))
 es-decls(es;"i";;rcv(lnk1{i to j},"tg") : T)
 @"i"[[[eclor(eclbase(A;s,v. tt).1;eclthrow(eclbase(B;s,v. tt);1))]*;A sends on lnk1{i to j}
 @"i"[[[eclor(eclbase(A;s,v. tt).1;eclthrow(eclbase(B;s,v. tt);1))]*;Awith tag "tg"
 @"i"[[[eclor(eclbase(A;s,v. tt).1;eclthrow(eclbase(B;s,v. tt);1))]*;A[s,v.m], at marker 1;]]
 es-sends-iff2(es;lnk1{i to j};"tg";T;;e.kind(e) = A
 & e[es-init(es;e),e].(kind(e) = B);e.m) 

latex

Definitions

deq-member(eq;x;L), x  dom(f), update-spec(ds;da), e loc e' , , A c B, e2 = first e  e1.P(e), ff, (i = j), if b then t else f fi , e[e1,e2).P(e), P  Q, False, P  Q, x,y. t(x;y), x. t(x), t  T, source(l), , IdLnk, Id, P  Q, Top, f(x)?z, t.1, Y, True, reduce(f;k;as), e[e1,e2].P(e), P & Q, tt, lnk$n{$a to $b}, , "$x", A, P  Q, Knd, x:A. B(x), x:A. B(x), b, i <z j, s-insert(x;l), (x  l), i z j, b, ecl-ex(x), ecl-es-halt(es;x), x(s), x(s1,s2), State(ds), ecl-es-act(es;m;x), t.2, fpf-domain(f), map(f;as), update-spec-vars(upd), msg-spec-links(snd), xL.P(x), k sends on l with tag tg [s,v.f(s;v)], at marker n, @i[[x;snd;upd]], x : v, es-decls(es;i;ds;da), [e1,e2]~([a,b].p(a;b))+

Lemmas

event system wf, rcv wf, fpf-single wf3, Id wf, es-decls wf, update-spec-empty-decl, msg-spec-loc-spec1, le wf, fpf-empty wf, Knd wf, IdLnk wf, ecl-mng wf, simplify-equal-imp, alle-between2 functionality wrt iff, duplicate-and, es-init-le, decidable equal Kind, es-pplus-first-since-exit, alle-between1-not-first-since, and true l, alle-between1-true, not-false, iff transitivity, and true r, es-first-since functionality wrt iff, or false r, and false l, es-pplus functionality wrt iff, es-pplus wf, es-interval wf, l member wf, or false l, not functionality wrt iff, alle-between1 functionality wrt iff, es-le-loc, es-locl wf, es-le wf, or functionality wrt iff, es-pstar-q functionality wrt iff, es-init wf, and functionality wrt iff, lsrc wf, es-E wf, false wf, not wf, alle-between1 wf, true wf, es-kind wf, es-first-since wf, es-loc wf, es-loc-init, es-pstar-q wf, es-sends-iff2 functionality, ma-valtype wf, Kind-deq wf, fpf-cap-single1, fpf-single wf, ecl-mng-sends-single2